(module typecore mzscheme
  (provide type-of-exp)
  (require "types/types.scm")
  (require "metadata.scm")
  (require "types/type-unification.scm")
  
  (define (type-of-push ty)
    (let ((fresh-var (fresh-tystackvar)))
      (make-ty-app (make-tycon-pure-arrow)
                   (list fresh-var (make-ty-app (make-tycon-cons)
                                                (list ty fresh-var))))))
  
  (define (apply-ty ty)
    (let ((ans-ty (fresh-tyvar)))
      ((substitute (unify 
                    (list (make-constraint 
                           (make-ty-app (make-tycon-pure-arrow)
                                        (list (make-ty-app 
                                               (make-tycon-null) (list))
                                              (make-ty-app
                                               (make-tycon-cons)
                                                (list ans-ty
                                                      (make-ty-app 
                                                       (make-tycon-null) (list))))))
                           ty)))) ans-ty)))
  
  (define (infer-list stx)
    (let ((elem-ty (fresh-tyvar)))
    (let loop ((stx         stx)
               (constraints (list)))
    (syntax-case stx ()
      (() (let ((ty-env (unify constraints)))
            (make-ty-app (make-tycon-list) (list ((substitute ty-env) elem-ty)))))
      ((elem elems ...)
       (let ((res-ty (apply-ty (type-of-exp #'(elem)))))
         (display res-ty)
         (if (and (ty-app? res-ty) (tycon-cons? (ty-app-tycon res-ty))
                  (ty-app? (cadr (ty-app-args res-ty)))
                  (tycon-null? (ty-app-tycon (cadr (ty-app-args res-ty)))))
             (loop #'(elems ...) (cons (make-constraint elem-ty (car (ty-app-args res-ty)))
                                       constraints))
             (raise-syntax-error #f "Expected list element to produce a single item." stx))))))))
  
  (define (cat-exp-to-type stx)
    (display stx)
    (syntax-case stx (lst)
      ((lst) (type-of-push (make-ty-app (make-tycon-list) (list (fresh-tyvar)))))
      ((lst xs ...) (type-of-push (infer-list #'(xs ...))))
      ((cmds ...) (type-of-push (type-of-exp #'(cmds ...))))
      (prim (and (identifier? #'prim) (cat-ref (syntax-e #'prim) #f))
            (cat-func-type (cat-ref (syntax-e #'prim)
                                    (lambda () (raise-syntax-error #f "undefined cat function/primitive" #'prim)))))
      (other (integer? (syntax-e #'other)) 
       (type-of-push (make-ty-app (make-tycon-int) (list))))
      (other 
       (type-of-push (make-ty-app (make-tycon-top) (list))))))
  
  (require "types/type-pprint.scm")
  ;; Helper function for type-of-exp
  (define (type-of-exp-helper ty stx)
    (syntax-case stx ()
      (() ty)
      ((prim exps ...)
        (let ((exp-ty (cat-exp-to-type #'prim)))
          (display (format "Type of ~S is ~S~%" (syntax-e #'prim) (type->string exp-ty)))
          (type-of-exp-helper (compose ty exp-ty) #'(exps ...))))))
  
  (define identity-type
    (make-ty-app (make-tycon-pure-arrow)
                 (list (make-ty-var 'S) (make-ty-var 'S))))
  
  (define (type-of-exp stx)
    (syntax-case stx ()
      ((cmds ...)
       (type-of-exp-helper identity-type (syntax->list #'(cmds ...))))))
  )